Termination w.r.t. Q proof of TRS/higher-order/LifantsevEx8Polymorphic.trs

Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

app(app(twice, f), x) → app(f, app(f, x))
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, h), t)) → app(app(cons, app(f, h)), app(app(map, f), t))
app(app(fmap, nil), x) → nil
app(app(fmap, app(app(cons, f), t_f)), x) → app(app(cons, app(f, x)), app(app(fmap, t_f), x))

Q is empty.

↳ QTRS

Q restricted rewrite system:
The TRS R consists of the following rules:

app(app(twice, f), x) → app(f, app(f, x))
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, h), t)) → app(app(cons, app(f, h)), app(app(map, f), t))
app(app(fmap, nil), x) → nil
app(app(fmap, app(app(cons, f), t_f)), x) → app(app(cons, app(f, x)), app(app(fmap, t_f), x))

Q is empty.